Inference at * 
Iof proof for Lemma connex iff trichot:


  T:Type, R:(TT).
  (a, b:T. Dec(R(a,b)))
   (Connex(T;x,y.R(x,y))
    {a, b:T.
    strict_part(x,y.R(x,y);a;b)
     Symmetrize(x,y.R(x,y);a;b)
     strict_part(x,y.R(x,y);b;a)}) 

latex

 by Unfold `guard` 0 

latex

 1: 

 1:   T:Type, R:(TT).
 1:   (a, b:T. Dec(R(a,b)))
 1:    (Connex(T;x,y.R(x,y))
 1:     (a, b:T.
 1:     strict_part(x,y.R(x,y);a;b)
 1:      Symmetrize(x,y.R(x,y);a;b)
 1:      strict_part(x,y.R(x,y);b;a)))
 .

Definitions

{T}